@Article{Leavens-Baker-Ruby06,
  Author =	 "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  Title =	 "Preliminary Design of {JML}: A Behavioral Interface Specification Language for {Java}",
  journal = "SIGSOFT",
  volume = 31,
  number = 3,
  month = mar,
  year = 2006,
  pages = {1-38},
  URL = {\url{http://doi.acm.org/10.1145/1127878.1127884}},
  publisher = "ACM",
}


@InProceedings{SpecSharp,
  Author="Mike Barnett and K. Rustan M. Leino and Wolfram Schulte",
  Title="The {Spec\#} programming system: An overview.",
  Booktitle="CASSIS",
  Year=2004,
  Series="LNCS",
  volume=3362,
  publisher="Springer",
}

@INPROCEEDINGS{Ball04slamand,
    author = {Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani},
    title = {{SLAM} and static driver verifier: Technology transfer of formal methods inside {Microsoft}},
    booktitle = {Integrated Formal Methods},
    year = {2004},
    pages = {1--20},
    publisher = {Springer}
}

@inproceedings{OpalDas06,
  author    = {Manuvir Das},
  title     = {Formal Specifications on Industrial-Strength Code-From Myth
               to Reality},
  booktitle = {Computer Aided Verification, 18th International Conference,
               CAV 2006},
  year      = {2006},
  pages     = {1},
}

@INPROCEEDINGS{Deline04typestatesfor,
    author = {Robert Deline and Manuel Fahndrich},
    title = {Typestates for Objects},
    booktitle = {Proceedings of the 18th European Conference on Object-Oriented Programming},
    year = {2004},
    pages = {465--490},
    publisher = {Springer}
}


@inproceedings{nonnull,
 author = {F\"{a}hndrich, Manuel and Leino, K. Rustan M.},
 title = {Declaring and checking non-null types in an object-oriented language},
 booktitle = {OOPSLA '03: Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications},
 year = {2003},
 pages = {302--312},
 publisher = {ACM},
 }

@inproceedings{pluggable,
 author = {Papi, Matthew M. and Ali, Mahmood and Correa,Jr., Telmo Luis and Perkins, Jeff H. and Ernst, Michael D.},
 title = {Practical pluggable types for {Java}},
 booktitle = {ISSTA '08: Proceedings of the 2008 international symposium on Software testing and analysis},
 year = {2008},
 pages = {201--212},
 publisher = {ACM},
}

@inproceedings{Dana,
  author    = {Dana N. Xu and
               Simon L. Peyton Jones and
               Koen Claessen},
  title     = {Static contract checking for {Haskell}},
  booktitle = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages},
  publisher = {ACM},
  year      = {2009},
  pages     = {41-52},
}

@inproceedings{DML,
 author = {Xi, Hongwei and Pfenning, Frank},
 title = {Dependent types in practical programming},
 booktitle = {POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1999},
 pages = {214--227},
 publisher = {ACM},
 }

@inproceedings{adaspark,
 author = {Carr\'{e}, Bernard and Garnsworthy, Jonathan},
 title = {{SPARK}---an annotated {Ada} subset for safety-critical programming},
 booktitle = {TRI-Ada '90: Proceedings of the conference on TRI-ADA '90},
 year = {1990},
 pages = {392--402},
 publisher = {ACM},
 }



@inproceedings{vcc,
  author    = {Markus Dahlweid and
               Michal Moskal and
               Thomas Santen and
               Stephan Tobies and
               Wolfram Schulte},
  title     = {{VCC}: Contract-based modular verification of concurrent {C}},
  booktitle = {31st International Conference on Software Engineering, ICSE
               2009, May 16-24, 2009, Vancouver, Canada, Companion Volume},
  year      = {2009},
  pages     = {429-430},
  publisher = {IEEE},
}


@Book{eiffel,
  author = 	 {Meyer, B{.}},
  title = 	 {Eiffel: {T}he {L}anguage},
  publisher = 	 {Prentice {H}all},
  year = 	 {1992}
}

@article{DBLP:journals/cacm/King76,
  author    = {James C. King},
  title     = {Symbolic Execution and Program Testing},
  journal   = {Communications of the ACM},
  volume    = {19},
  number    = {7},
  year      = {1976},
  pages     = {385-394},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  abstract = {This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program (e.g. numbers) one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be symbolic formulas over the input symbols. The difficult, yet interesting issues arise during the symbolic execution of conditional branch type statements. A particular system called EFFIGY which provides symbolic execution for program testing and debugging is also described. It interpretively executes programs written in a simple PL/I style programming language. It includes many standard debugging features, the ability to manage and to prove things about symbolic expressions, a simple program testing manager, and a program verifier. A brief discussion of the relationship between symbolic execution and program proving is also included. } }


@article{DBLP:journals/tse/Korel90,
  author    = {Bogdan Korel},
  title     = {Automated Software Test Data Generation},
  journal   = {IEEE Transactions on Software Engineering},
  volume    = {16},
  number    = {8},
  year      = {1990},
  pages     = {870-879},
  ee        = {http://www.computer.org/tse/ts1990/e0870abs.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de} }


@inproceedings{DBLP:conf/kbse/GuptaMS00,
  author    = {Neelam Gupta and
               Aditya P. Mathur and
               Mary Lou Soffa},
  title     = {Generating Test Data for Branch Coverage},
  booktitle = {ASE : IEEE International Conference on Automated Software Engineering},
  year      = {2000},
  pages     = {219-228},
  ee        = {http://computer.org/proceedings/ase/0710/07100219abs.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  abstract = { Branch coverage is an important criteria used during the structural testing of programs. In this paper, we present a new program execution based approach to generate input data that exercises a selected branch in a program. The test data generation is initiated with an arbitrarily chosen input from the input domain of the program. A new input is derived from the initial in-put in an attempt to force execution through any of the paths through the selected branch. The method dynamically switches among the paths that reach the branch by refining the input. Using a numerical iterative technique that attempts to generate an input to exercise the branch, it dynamically selects a path that offers less resistance. We have implemented the technique and present experimental results of its performance for some programs. Our results show that our method is feasible and practical. } }

@inproceedings{DBLP:conf/popl/Godefroid07,
  author    = {Patrice Godefroid},
  title     = {Compositional dynamic test generation},
  booktitle = {Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  year      = {2007},
  pages     = {47-54},
  ee        = {http://doi.acm.org/10.1145/1190216.1190226},
  bibsource = {DBLP, http://dblp.uni-trier.de} }


@inproceedings{DBLP:conf/tap/TillmannH08,
  author    = {Nikolai Tillmann and
               Jonathan de Halleux},
  title     = {Pex-White Box Test Generation for {.NET}},
  booktitle = {TAP: Tests and Proofs Second International Conference},
  year      = {2008},
  pages     = {134-153},
  ee        = {http://dx.doi.org/10.1007/978-3-540-79124-9_10},
  bibsource = {DBLP, http://dblp.uni-trier.de} }


@inproceedings{datagroups,
 author = {Leino, K. Rustan M.},
 title = {Data groups: specifying the modification of extended state},
 booktitle = {OOPSLA '98: Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications},
 year = {1998},
 pages = {144--153},
 }


@InProceedings{LogozzoMaf08-2,
  author = 	 {Logozzo, F{.} and F\"ahndrich, M{.} A{.}},
  title = 	 {On the Relative Completeness of Bytecode Analysis versus Source Code Analysis},
  booktitle = {CC'08},
  year = 	 {2008},
  series = 	 {LNCS},
  month = 	 mar,
  publisher = {Springer-Verlag}
}

@InProceedings{LogozzoMaf08,
  author = {Logozzo, F{.} and F\"ahndrich, M{.} A{.}},
  title = {Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses},
  booktitle = {ACM SAC'08 - OOPS},
  month = mar,
  year = 2008,
  publisher = {ACM Press}
}
